COMMENT ⊗   VALID 00004 PAGES 
RECORD PAGE   DESCRIPTION
 00001 00001
 00002 00002	
 00004 00003	
 00005 00004	
 00006 ENDMK
⊗;


There are actually three interwoven parsers all constructed by Lynn Quam's
Syntax Directed Input Output program.  The parsers are for the programmable
prover, the input language, and for the command language.

The most simple parser extends LISP  to recognize the new data types: strategies,
patterns and clauses.  Please note that in this language <alt-mode> is not recognized.

.BEGIN VERBATIM

<EXP>   ::=<ATOM>
	::=[<REM>]
	::=(<LST>)

<LST>   ::=<EXP><LST>
	::=

<REM>   ::=CHOICE<ST>
	::=DECLARE<DECOP>:<OPLIST>
	::=EDIT<ST>
	::=CLAUSES<CLAUSES>
	::=PATTERN<F1>

.END



<PREDIC>::=ANCESTRY
	::=NONE
	::=VINE
	::=UNIT
	::=P1
	::=P2
	::=SUPPORT[<C>]
	::=MODEL[<PREDLST>;<PREDLST>]
	::=EQUALITY[<OP>,<NUMBER>]
	::=DEMOD[<CLAUSES>,<NUMBER>]
	::=DEFMODEL[ID]
	::=@<LISPR>
	::=<TERM><OPR><TERM>

<PREDLST>
	::=<ID>,<PREDLST>
	::=<ID>
	::=




The routines corresponding to <PREPREDLET>, <INFPREDLET>, <IVAR>, <PREFN>, and
<INFN> check the lists of prefix- and infix- predicate and function letters, and
the variable list, all of which were manufactured by the appropriate declarations.

.BEGIN VERBATIM

<PRED>  ::=<PREPREDLET><ITMLST>
	::=<TM><INFPREDLET><TM>

<ITMLST>::=(<ITMS>

<ITMS>  ::=<TM><ITMS>
	::=<TM>)

<TM>    ::=<IVAR>
	::=<PREFN><ITMLST>
	::=<PREFN>
	::=(<TM>)
	::=<TM><INFN><TM>
.END